Nuprl Definition : non-void-decl
11,40
postcript
pdf
non-void(
d
) ==
x
dom(
d
).
A
=
d
(
x
)
A
latex
clarification:
non-void-decl(
T
;
eq
;
d
) ==
T
eq
x
dom(
d
).
A
=
d
(
x
)
A
latex
Definitions
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
FDL editor aliases
non-void-decl
origin
x
dom(d). A=d(x) 
A
xdom(d). A=d(x) A xdom(d). A=d(x) A
xdom(d). A=d(x) A xdom(f). v=f(x) P(x;v)